1. $P$ : $\mathbb{P}$ \\[0ex]2. $d$ : Dec($P$) \\[0ex]3. $\uparrow$[$d$]$_{b}$ \\[0ex]$\vdash$ $P$